package com.solver.demo.smt.main;

import org.sosy_lab.java_smt.api.*;

public class SmtExample {

    public static void main(String[] args) throws Exception {
        test();
    }

    public static void test() throws Exception {
        /**
         * 创建一个 Solver 上下文
         * todo
         * 这个地方有个疑问？
         * SmtSolverUtil.solverContext方法虽然不用每次都加载z3引擎，但是需要每次都create  Configuration LogManager和ShutdownNotifier，是否合理？
         */
        SolverContext context = SmtSolverUtil.solverContext();

        FormulaManager fmgr = context.getFormulaManager();
        BooleanFormulaManager booleanMgr = fmgr.getBooleanFormulaManager();
        IntegerFormulaManager intMgr = fmgr.getIntegerFormulaManager();


        // 创建一些变量
        NumeralFormula.IntegerFormula x = intMgr.makeVariable("x");
        NumeralFormula.IntegerFormula y = intMgr.makeVariable("y");

        // 添加额外的约束 x = 3 和 y = 7
        BooleanFormula xEquals3 = intMgr.equal(x, intMgr.makeNumber(3));
        BooleanFormula yEquals7 = intMgr.equal(y, intMgr.makeNumber(7));

        // 创建公式 x + y = 10
        BooleanFormula equation = intMgr.equal(intMgr.add(x, y), intMgr.makeNumber(10));

        // 创建公式 x > 0 and y > 0
        BooleanFormula constraints = booleanMgr.and(intMgr.greaterThan(x, intMgr.makeNumber(0)),
                intMgr.greaterThan(y, intMgr.makeNumber(0)));

        // 合并所有约束，包括具体值
        BooleanFormula specificValueConstraints = booleanMgr.and(constraints, xEquals3, yEquals7);

        // 合并所有约束
        BooleanFormula formula = booleanMgr.and(equation, constraints, specificValueConstraints);

        // 检查公式是否可满足
        try (ProverEnvironment prover = context.newProverEnvironment()) {
            prover.addConstraint(formula);
            if (prover.isUnsat()) {
                System.out.println("The formula is unsatisfiable.");
            } else {
                System.out.println("The formula is satisfiable.");
            }
        }
    }
}
